constructive mathematics, realizability, computability
propositions as types, proofs as programs, computational trinitarianism
internalization and categorical algebra
algebra object (associative, Lie, …)
natural deduction metalanguage, practical foundations
type theory (dependent, intensional, observational type theory, homotopy type theory)
computational trinitarianism =
propositions as types +programs as proofs +relation type theory/category theory
In computer science, an exception is a nominal failure of a program which however is handled in some manner, so that the failing computation still terminates in a controlled way.
In the simplest case this may mean that the program outputs an error message instead of continuing with the intended computation.
In terms of monads in computer science, the effect of (possibly) throwing an exception is modeled by the monad:
which turns a given output data type into the coproduct type
with the intended type of handling/messages (typically string);
whose bind-operation on any is given by the codiagonal map as
meaning that whatever exception message has already been thrown gets carried further along.
If here is the unit type, then the exception monad is also known as the maybe monad, modelling the effect that a program may fail, without however transmitting any further information about the failure.
Exception monads correspond to coreader comonads in the opposite category, because coproducts turn into products there.
Exceptions monads in computer science:
Eugenio Moggi, Exp. 1.1 in: Notions of computation and monads, Information and Computation, 93 1 (1991) [doi:10.1016/0890-5401(91)90052-4, pdf]
Philip Wadler, §2.2 in: Monads for functional programming, in M. Broy (eds.) Program Design Calculi NATO ASI Series, 118 Springer (1992) [doi;10.1007/978-3-662-02880-3_8, pdf]
Jiří Adámek, Stefan Milius, Nathan Bowler, Paul B. Levy, Coproducts of Monads on Set, 27th Annual IEEE Symposium on Logic in Computer Science (2012) [arXiv:1409.3804, doi:10.1109/LICS.2012.16]
and on exception handling modales:
Lecture notes:
See also:
Last revised on February 6, 2024 at 22:48:29. See the history of this page for a list of all contributions to it.